perm filename XRED.XGP[1,JRA] blob sn#541169 filedate 1980-10-11 generic text, type T, neo UTF8
/LMAR=0/XLINE=4/FONT#1=BAXL30/FONT#0=BAXI30[  P,JRA]/FONT#2=BAXB30/FONT#3=NGR25/FONT#4=BAXI27/FONT#5=BAXL27/FONT#6=BAXB27/FONT#7=SUP/FONT#8=SPEC[  P,JRA]/FONT#9=BDR40/FONT#10=MATH30/FONT#11=METSB/FONT#12=NONMBI/FONT#13=GERM35/FONT#16=NGB30/FONT#15=ZERO30
␈↓ α␈↓␈↓ 
∀␈↓CONTENTS  ␈↓

␈↓"β␈↓ α␈↓	pub is a crock
␈↓ α␈↓␈↓ 
␈↓CONTENTS  i␈↓

␈↓"β␈↓ α␈↓	pub is more of a crock
␈↓ α␈↓␈↓ 
␈↓CONTENTS  i␈↓

␈↓"β␈↓ α␈↓	page it
␈↓ α␈↓␈↓ 
α␈↓CONTENTS  ii␈↓








␈↓ α␈↓	␈↓ βvT A B L E   O F   C O N T E N T S
␈↓ α␈↓␈↓ λ,␈↓  ␈↓
␈↓ α␈↓␈↓ λ␈↓  1␈↓

␈↓"β␈↓ α␈↓␈↓ ∧9␈↓αRunnable Specification As a Design Tool␈↓↓


␈↓"β␈↓ α␈↓↓␈↓ ¬tRuth E. Davis
␈↓"β␈↓ α␈↓↓␈↓ β\Electrical Engineering and Computer Science Department
␈↓"β␈↓ α␈↓↓␈↓ ¬*University of Santa Clara
␈↓"β␈↓ α␈↓↓␈↓ ¬;Santa Clara, CA 95053






␈↓"β␈↓ α␈↓␈↓↓There are at least four phases in the development of "correct" software.

␈↓"β␈↓ α␈↓↓␈↓ αH1)␈αUnderstanding␈α
the␈αproblem.␈α
 The␈αprogram␈α
designer␈αmay␈α
work␈αwith␈αintended␈α
users
␈↓ α␈↓↓of␈α⊗the␈α⊗system␈α↔to␈α⊗develop␈α⊗an␈α⊗intuitive␈α↔understanding␈α⊗of␈α⊗the␈α⊗problem␈α↔and␈α⊗possible
␈↓ α␈↓↓approaches to its solution.

␈↓"β␈↓ α␈↓↓␈↓ αH2)␈α∀Formal␈α∀specification.␈α∪ Once␈α∀the␈α∀designer␈α∀knows␈α∪intuitively␈α∀how␈α∀to␈α∀solve␈α∪the
␈↓ α␈↓↓problem, the solution must be specified unambiguously.

␈↓"β␈↓ α␈↓↓␈↓ αH3) Programming.  An implementation of the specification is programmed.

␈↓"β␈↓ α␈↓↓␈↓ αH4)␈α
Verification.␈α The␈α
implementation␈αdeveloped␈α
in␈αstep␈α
three␈αis␈α
shown␈αto␈α
satisfy␈αthe
␈↓ α␈↓↓formal specification of step two.

␈↓"β␈↓ α␈↓↓␈↓ αHThere␈α∞is␈α∂a␈α∞certain␈α∂amount␈α∞of␈α∞testing␈α∂and␈α∞debugging␈α∂that␈α∞goes␈α∞on␈α∂at␈α∞each␈α∂of␈α∞these
␈↓ α␈↓↓stages␈α⊃until␈α⊃one␈α⊃is␈α⊃satisfied␈α⊃with␈α⊃the␈α⊂current␈α⊃step␈α⊃and␈α⊃moves␈α⊃on␈α⊃to␈α⊃the␈α⊃next.␈α⊂ Several
␈↓ α␈↓↓verification␈α
techniques␈α
have␈α
been␈α
developed␈α
to␈α
assist␈α
in␈α
accomplishing␈α
step␈α
four.␈α
 However,
␈↓ α␈↓↓even␈αafter␈αa␈αproof␈αis␈α
completed␈αwe␈αcannot␈αclaim␈αto␈α
have␈αa␈α"correct"␈αprogram,␈αonly␈αone␈α
that
␈↓ α␈↓↓satisfies the given specification.

␈↓"β␈↓ α␈↓↓␈↓ αHRather␈α∞than␈α∞write␈α∞a␈α∞program,␈α∞being␈α
guided␈α∞by␈α∞the␈α∞specification,␈α∞and␈α∞then␈α∞prove␈α
it
␈↓ α␈↓↓satisfies␈α
the␈α
specifications,␈α
one␈α
can␈α
automatically␈α
generate␈α
a␈α
program␈α
from␈α
the␈α
specifications
␈↓ α␈↓↓that␈α
is␈α
guaranteed␈α
to␈α
preserve␈α
the␈α∞semantics,␈α
thus␈α
obviating␈α
the␈α
need␈α
for␈α∞the␈α
verification
␈↓ α␈↓↓step entirely [1].

␈↓"β␈↓ α␈↓↓␈↓ αHThe␈α
truly␈α
creative␈α
(and␈α
most␈α
difficult)␈α
step␈α
in␈α
the␈α
development␈α
of␈α
a␈α
program␈α∞is␈α
the
␈↓ α␈↓↓construction␈α
of␈α
an␈α
acceptable␈α
formal␈α∞specification␈α
from␈α
an␈α
intuitive␈α
understanding␈α∞of␈α
the
␈↓ α␈↓↓problem.␈α
 Thus,␈αour␈α
efforts␈α
should␈αbe␈α
placed␈α
on␈αdeveloping␈α
design␈α
tools␈αto␈α
help␈α
with␈αthe
␈↓ α␈↓↓construction and testing of the specification.

␈↓"β␈↓ α␈↓↓␈↓ αHHow␈α∂does␈α∂one␈α∂"debug"␈α∂a␈α∂specification?␈α∂ We␈α∂cannot␈α∂hope␈α∂to␈α∂formally␈α∂prove␈α∂that␈α∂a
␈↓ α␈↓↓specification␈α
is␈α
"correct"␈α
with␈α
respect␈α
to␈α
our␈α
intuition,␈αbut␈α
we␈α
can␈α
at␈α
least␈α
test␈α
it␈α
to␈α
see␈αthat␈α
it
␈↓ α␈↓↓conforms to our intuition in specific cases.
␈↓ α␈↓␈↓ β␈↓  2␈↓

␈↓"β␈↓ α␈↓↓␈↓ αHGuttag␈αand␈αHorning␈α[2]␈αpresent␈αan␈αalgebraic␈αspecification␈αtechnique␈αas␈αa␈αdesign␈αtool.
␈↓ α␈↓↓As␈αan␈α
example␈αthey␈α
describe␈αpart␈α
of␈αthe␈α
specification␈αof␈α
a␈αhigh-level␈α
interface␈αto␈αa␈α
flexible
␈↓ α␈↓↓display␈αand␈αdiscuss␈αthe␈αanalysis␈αof␈αthe␈αspecification.␈α A␈αsalient␈αfeature␈αof␈αtheir␈αapproach␈αis
␈↓ α␈↓↓the␈αability␈αto␈α"ask␈αquestions"␈αof␈αthe␈αspecification,␈αderive␈αanswers,␈αand␈αchange␈αthe␈αdesign␈αif
␈↓ α␈↓↓the answers are unacceptable.  In this way they hope to test and debug the specification.

␈↓"β␈↓ α␈↓↓␈↓ αHI␈α∂suggest␈α∂that␈α⊂Horn␈α∂clauses␈α∂provide␈α∂a␈α⊂much␈α∂better␈α∂specification␈α∂language␈α⊂than␈α∂do
␈↓ α␈↓↓algebraic␈α
axioms.␈α The␈α
two␈αlanguages␈α
are␈α
closely␈αrelated;␈α
it␈αis␈α
a␈αsimple␈α
matter␈α
to␈αtranslate
␈↓ α␈↓↓between␈α∂them.␈α∂ The␈α∂ease␈α⊂of␈α∂writing␈α∂a␈α∂specification␈α∂in␈α⊂one␈α∂language␈α∂versus␈α∂the␈α⊂other␈α∂is
␈↓ α␈↓↓undoubtedly␈α
a␈αmatter␈α
of␈αpersonal␈α
taste␈αand␈α
depends␈α
largely␈αon␈α
which␈αlanguage␈α
one␈αis␈α
more
␈↓ α␈↓↓familiar␈α
with.␈α
 The␈α
same␈α
may␈α
be␈α
said␈αof␈α
the␈α
readability␈α
of␈α
a␈α
specification.␈α
 Horn␈αclauses,␈α
as
␈↓ α␈↓↓well␈α
as␈α∞algebraic␈α
axioms,␈α
can␈α∞be␈α
analyzed␈α∞for␈α
answers␈α
to␈α∞specific␈α
questions␈α∞and␈α
modified
␈↓ α␈↓↓accordingly.

␈↓"β␈↓ α␈↓↓␈↓ αHThe␈α
major␈α
distinction␈α
between␈α
the␈α
two␈α
methods␈α
is␈α
the␈α
manner␈α
in␈α
which␈αquestions␈α
can
␈↓ α␈↓↓be␈α∩handled.␈α∩ With␈α∩the␈α∩Guttag-Horning␈α∩approach,␈α∩an␈α∩informal␈α∩question␈α∩is␈α∩posed␈α⊃and
␈↓ α␈↓↓submitted␈α∃to␈α⊗an␈α∃"expert"␈α⊗who␈α∃reformulates␈α⊗the␈α∃question,␈α⊗often␈α∃generalizing␈α⊗it.␈α∃The
␈↓ α␈↓↓questioner␈αmust␈αthen␈αbe␈αconvinced␈αthat␈αthe␈αformal␈αstatement␈αdeveloped␈αby␈αthe␈αexpert␈αdoes
␈↓ α␈↓↓indeed␈αreflect␈αthe␈αoriginal␈αquestion,␈αand␈αan␈αanswer␈αto␈αthe␈αformal␈αquestion␈αwill␈αprovide␈αan
␈↓ α␈↓↓answer␈α∂to␈α∂the␈α∂informal␈α∂one.␈α∂ Finally,␈α∂an␈α∞attempt␈α∂is␈α∂made␈α∂to␈α∂derive␈α∂an␈α∂answer␈α∂from␈α∞the
␈↓ α␈↓↓axioms.

␈↓"β␈↓ α␈↓↓␈↓ αHThe␈α
same␈α
approach␈α
may␈α
be␈α
taken␈α
with␈α
Horn␈α
clauses,␈α
but␈α
it␈α
is␈α
not␈α
necessary.␈α
 Since
␈↓ α␈↓↓Horn␈αclauses␈αare␈αexecutable,␈αif␈αthe␈αquestioner␈αwants␈αto␈αknow␈αwhat␈αhappens␈αin␈αa␈αparticular
␈↓ α␈↓↓case,␈αit␈αis␈αpossible␈αto␈αsimply␈α"try␈αit␈αand␈αsee".␈αThe␈αexpert␈αwill␈αstill␈αbe␈αneeded␈αto␈αdevelop␈αthe
␈↓ α␈↓↓specification␈α
and␈α∞to␈α
determine␈α∞what␈α
modifications␈α
should␈α∞be␈α
made␈α∞to␈α
the␈α∞specification␈α
to
␈↓ α␈↓↓change␈αan␈αunacceptable␈αanswer,␈αbut␈αthe␈α"what␈αhappens␈αif␈α...?"␈αquestions␈αno␈αlonger␈αneed␈αbe
␈↓ α␈↓↓formalized.␈α For␈αexample,␈αgiven␈αthe␈αspecification␈αdetailed␈αin␈αthe␈αappendix,␈αand␈αdefinitions
␈↓ α␈↓↓for␈α∀the␈α∃primitives␈α∀(machine␈α∀dependent)␈α∃that␈α∀interface␈α∀the␈α∃underlying␈α∀logic␈α∃with␈α∀the
␈↓ α␈↓↓commands␈αcontrolling␈αthe␈αappearance␈αof␈αthe␈αscreen,␈αit␈αis␈αpossible␈αto␈αexecute␈αlogic␈αprograms
␈↓ α␈↓↓that␈αmanipulate␈αthe␈αdisplay.␈α Ideally,␈αa␈α"front-end"␈αcommand␈αlanguage␈αshould␈αbe␈α
provided
␈↓ α␈↓↓by␈α∂the␈α∂designer(s)␈α⊂that␈α∂enables␈α∂users/testers␈α⊂of␈α∂the␈α∂design␈α∂to␈α⊂make␈α∂their␈α∂requests␈α⊂of␈α∂the
␈↓ α␈↓↓system without having to write them as Horn clauses.

␈↓"β␈↓ α␈↓↓␈↓ αHOnce␈αone␈αis␈αsatisfied␈αthat␈αa␈αHorn␈αclause␈αspecification␈αis␈αa␈αreasonable␈αembodiment␈αof
␈↓ α␈↓↓one's␈αintuition,␈αthe␈αtask␈αof␈αrefining␈αthe␈αspecification␈αinto␈αan␈αefficient␈αprogram␈αcan␈αproceed.
␈↓ α␈↓↓The␈α∞ability␈α∂to␈α∞run␈α∂a␈α∞specification␈α∂makes␈α∞the␈α∞problem␈α∂of␈α∞testing␈α∂and␈α∞debugging␈α∂it␈α∞much
␈↓ α␈↓↓more tractable.

␈↓"β␈↓ α␈↓↓␈↓ αHAs␈αan␈αexample,␈αI␈α
have␈αwritten␈αthe␈αHorn␈α
clause␈αspecification␈αof␈αthe␈α
display␈αspecified
␈↓ α␈↓↓with␈α∂algebraic␈α∂axioms␈α∂by␈α∂Guttag␈α∂and␈α∂Horning.␈α∂ The␈α∂fundamental␈α∂assumption␈α∂is␈α⊂that␈α∂a
␈↓ α␈↓↓user␈αwill␈αwant␈αto␈αbe␈αable␈αto␈αdisplay␈αseveral␈αdistinct␈αblocks␈αof␈αinformation␈αon␈αthe␈αscreen␈αat
␈↓ α␈↓↓once.␈α
 The␈α
top␈αlevel␈α
concept␈α
is␈α
that␈αof␈α
a␈α
␈↓view␈↓↓.␈αA␈α
␈↓view␈↓↓␈α
is␈α
a␈αspatial␈α
arrangement␈α
of␈α␈↓pictures␈↓↓;␈α
a
␈↓ α␈↓↓␈↓picture␈↓↓␈αis␈αa␈αblock␈αof␈αdisplayable␈αinformation.␈αA␈αpicture␈αconsists␈αof␈αa␈αboundary,␈αa␈αcontents,
␈↓ α␈↓↓and␈α
a␈α
coordinate␈α
transformation␈αto␈α
be␈α
applied␈α
in␈αviewing␈α
its␈α
contents.␈α
Examples␈αof␈α
pictures
␈↓ α␈↓↓are␈αthe␈αentire␈αdisplay␈α(with␈αimplicit␈αboundary),␈α
and␈αthe␈αinterior␈αof␈αa␈αfixed␈αrectangle␈αon␈α
the
␈↓ α␈↓↓display;␈α∂examples␈α⊂of␈α∂contents␈α⊂are␈α∂text,␈α∂figures,␈α⊂and␈α∂views.␈α⊂Figure␈α∂1␈α∂is␈α⊂an␈α∂example␈α⊂of␈α∂a
␈↓ α␈↓␈↓ α␈↓  3␈↓

␈↓"β␈↓ α␈↓↓picture␈α(or␈α
a␈αview␈α
containing␈αa␈α
single␈αpicture).␈α Figure␈α
2␈αpresents␈α
a␈αview␈α
containing␈αthree
␈↓ α␈↓↓pictures,␈α⊂each␈α∂of␈α⊂which␈α∂has␈α⊂the␈α⊂same␈α∂contents;␈α⊂they␈α∂differ␈α⊂in␈α∂their␈α⊂boundaries␈α⊂and␈α∂the
␈↓ α␈↓↓coordinate transformations applied in viewing their contents.

␈↓"β␈↓ α␈↓↓␈↓ αHThe Guttag-Horning specification of picture is as follows:

␈↓"β␈↓ α␈↓↓␈↓ αH␈↓∧Operators:

␈↓"β␈↓ α␈↓∧␈↓ αHMakePicture: Contents ␈↓βX␈↓∧ [Coordinate → TruthValues] ␈↓βX␈↓∧ [Coordinate → Coordinate]
␈↓"β␈↓ α␈↓∧␈↓ αH                                 → Picture

␈↓"β␈↓ α␈↓∧␈↓ αHPicture.Appearance: Picture ␈↓βX␈↓∧ Coordinate → Illumination

␈↓"β␈↓ α␈↓∧␈↓ αHPicture.In: Picture ␈↓βX␈↓∧ Coordinate → TruthValues

␈↓"β␈↓ α␈↓∧␈↓ αHAxioms:

␈↓"β␈↓ α␈↓∧␈↓ αHPicture.Appearance(MakePicture(cont, bound, trans), coord)
␈↓"β␈↓ α␈↓∧␈↓ αH                                        ␈↓=␈↓∧ Contents.Appearance(cont, trans(coord))

␈↓"β␈↓ α␈↓∧␈↓ αHPicture.In(MakePicture(cont, bound, trans), coord) ␈↓=␈↓∧ bound(coord)


␈↓"β␈↓ α␈↓↓␈↓ αHThe␈α⊂operators␈α∂are␈α⊂listed␈α∂first,␈α⊂giving␈α∂their␈α⊂functionality,␈α∂then␈α⊂the␈α⊂axioms␈α∂defining
␈↓ α␈↓↓them␈α⊃are␈α⊃given.␈α⊂ ␈↓MakePicture␈↓↓␈α⊃is␈α⊃not␈α⊂defined␈α⊃further␈α⊃since␈α⊂it␈α⊃is␈α⊃simply␈α⊃the␈α⊂constructor
␈↓ α␈↓↓function␈α∂for␈α⊂the␈α∂type␈α⊂␈↓Picture␈↓↓.␈α∂ The␈α∂first␈α⊂axiom␈α∂tells␈α⊂us␈α∂that␈α∂the␈α⊂appearance␈α∂at␈α⊂a␈α∂given
␈↓ α␈↓↓coordinate␈α⊂in␈α⊂a␈α⊂␈↓picture␈↓↓␈α⊂is␈α⊂determined␈α⊂by␈α⊂the␈α⊂appearance␈α⊂at␈α⊂a␈α⊂coordinate␈α⊂(the␈α⊃result␈α⊂of
␈↓ α␈↓↓applying␈αthe␈αtransformation␈αto␈αthe␈αoriginal␈αcoordinate)␈αin␈αthe␈α␈↓contents␈↓↓␈αof␈αthe␈α␈↓picture␈↓↓.␈α The
␈↓ α␈↓↓second␈αaxiom␈αindicates␈αthat␈αa␈αcoordinate␈αis␈αin␈αa␈α␈↓picture␈↓↓␈αif␈αit␈αis␈αwithin␈αthe␈αboundary␈αof␈αthe
␈↓ α␈↓↓␈↓picture␈↓↓ as defined by the function ␈↓bound␈↓↓.

␈↓"β␈↓ α␈↓↓␈↓ αHThe␈αspecification␈α
of␈αtype␈α
␈↓Picture␈↓↓␈αusing␈αHorn␈α
clauses␈αis␈α
given␈αbelow.␈α
We␈αdistinguish
␈↓ α␈↓↓predicate␈αnames␈αby␈αcapitalizing␈αthe␈αfirst␈α
letter,␈αconstants␈αand␈αfunction␈αsymbols␈αare␈α
give␈αin
␈↓ α␈↓↓bold␈α∪type,␈α∪and␈α∪variables␈α∪are␈α∪lower␈α∪case␈α∪italics.␈α∪The␈α∪Horn␈α∪clause␈α∪specification␈α∩clearly
␈↓ α␈↓↓indicates␈α∩the␈α∩distinction␈α∩between␈α∩constructor␈α∩functions,␈α∩such␈α∩as␈α∩␈↓αmake-picture␈↓↓,␈α∩and␈α⊃the
␈↓ α␈↓↓predicates␈αindicating␈αrelationships␈αamong␈αtheir␈αarguments.␈αThe␈αtype␈αconstraints,␈αindicating
␈↓ α␈↓↓functionality␈α⊂of␈α⊂the␈α⊂predicates,␈α⊂are␈α⊂given␈α∂only␈α⊂for␈α⊂the␈α⊂clause(s)␈α⊂defining␈α⊂the␈α⊂type␈α∂being
␈↓ α␈↓↓specified.␈α
 Type-checking␈α
can␈α
be␈α
included␈α
explicitly␈α
in␈α
each␈α
clause,␈α
however,␈α
we␈αassume␈α
the
␈↓ α␈↓↓required␈αtype␈α
is␈αmade␈αobvious␈α
by␈αconsistent␈α
naming␈αof␈αvariables␈α
and␈αchoose␈α
to␈αleave␈αit␈α
out
␈↓ α␈↓↓of the rest of the specification for the sake of readability.


␈↓"β␈↓ α␈↓↓␈↓ αH␈↓∧Picture(␈↓εmake-picture␈↓∧(cont, bound, trans)) ← Contents(cont), Boundary(bound),
␈↓"β␈↓ α␈↓∧␈↓ αH                                                Translation(trans)

␈↓"β␈↓ α␈↓∧␈↓ αHPicture-Appearance(␈↓εmake-picture␈↓∧(cont, bound, trans), coord, illum) ←
␈↓"β␈↓ α␈↓∧␈↓ αH        Compute-position(coord, trans, coord'), Contents-appearance(cont, coord', illum)

␈↓"β␈↓ α␈↓∧␈↓ αHPicture-In(␈↓εmake-picture␈↓∧(cont, bound, trans), coord, tv) ← Lies-in(coord, bound, tv)
␈↓ α␈↓␈↓ ¬␈↓  4␈↓

␈↓"β␈↓ α␈↓↓␈↓ αHIn␈α∀the␈α∃Guttag-Horning␈α∀axiomatic␈α∀specification␈α∃of␈α∀the␈α∀display,␈α∃a␈α∀␈↓boundary␈↓↓␈α∃is␈α∀a
␈↓ α␈↓↓function␈αfrom␈α
␈↓Coordinate␈↓↓␈αto␈α␈↓TruthValues␈↓↓␈α
and␈αa␈α
␈↓translation␈↓↓␈αis␈αa␈α
function␈αfrom␈α␈↓Coordinate␈↓↓␈α
to
␈↓ α␈↓↓␈↓Coordinate␈↓↓.␈α∞ Horn␈α∂clause␈α∞syntax␈α∂does␈α∞not␈α∞allow␈α∂functions␈α∞as␈α∂arguments,␈α∞thus␈α∂I've␈α∞treated
␈↓ α␈↓↓␈↓trans␈↓↓␈α↔and␈α⊗␈↓bound␈↓↓␈α↔as␈α⊗objects,␈α↔␈↓Compute-position␈↓↓␈α⊗is␈α↔a␈α⊗predicate␈α↔that␈α↔accomplishes␈α⊗the
␈↓ α␈↓↓translation␈α_from␈α_␈↓coord␈↓↓␈α_to␈α→␈↓coord'␈↓↓␈α_indicated␈α_by␈α_the␈α_Guttag-Horning␈α→␈↓trans␈↓↓,␈α_similarly,
␈↓ α␈↓↓␈↓Lies-in(coord,␈α→bound,␈α~tv)␈↓↓␈α→results␈α→in␈α~␈↓tv␈↓↓␈α→being␈α→bound␈α~to␈α→␈↓αtrue␈↓↓␈α→if␈α~and␈α→only␈α~if␈α→the
␈↓ α␈↓↓Guttag-Horning␈α⊗␈↓bound(coord)␈↓↓␈α⊗is␈α↔␈↓αtrue␈↓↓,␈α⊗and␈α⊗to␈α⊗␈↓αfalse␈↓↓␈α↔if␈α⊗and␈α⊗only␈α↔if␈α⊗Guttag-Horning
␈↓ α␈↓↓␈↓bound(coord)␈↓↓␈α∞is␈α
␈↓αfalse␈↓↓.␈α∞ I␈α
would␈α∞not␈α
need␈α∞the␈α
predicates␈α∞␈↓Compute-position␈↓↓␈α
and␈α∞␈↓Lies-in␈↓↓␈α∞if␈α
I
␈↓ α␈↓↓had␈α⊂an␈α∂evaluation␈α⊂predicate␈α∂that␈α⊂accepts␈α∂a␈α⊂function␈α∂and␈α⊂its␈α∂arguments␈α⊂and␈α⊂applies␈α∂the
␈↓ α␈↓↓function␈α∂to␈α∂the␈α∂arguments,␈α∂such␈α∂as␈α∂the␈α∞LISP␈α∂"apply".␈α∂ I␈α∂have␈α∂decided␈α∂to␈α∂remain␈α∞within
␈↓ α␈↓↓first-order␈α∃logic␈α∃and␈α∃the␈α∃strict␈α∃limitations␈α∃of␈α∃Horn␈α∃clauses.␈α∃ Others␈α∃have␈α∀concerned
␈↓ α␈↓↓themselves␈α∂with␈α∂the␈α∞problem␈α∂of␈α∂moving␈α∞to␈α∂second-order,␈α∂as␈α∞shown␈α∂in␈α∂the␈α∞"demonstrate"
␈↓ α␈↓↓predicate used of R. Kowalski and K. Bowen described in [3].

␈↓"β␈↓ α␈↓↓␈↓ αHThe specification of type ␈↓View␈↓↓, given algebraically, is as follows:


␈↓"β␈↓ α␈↓↓␈↓ αH␈↓∧Operators:

␈↓"β␈↓ α␈↓∧␈↓ αHView.Empty: → View

␈↓"β␈↓ α␈↓∧␈↓ αHAddPicture: View ␈↓βX␈↓∧ Coordinate ␈↓βX␈↓∧ PictureId ␈↓βX␈↓∧ Picture → View

␈↓"β␈↓ α␈↓∧␈↓ αHView.Appearance: View ␈↓βX␈↓∧ Coordinate → Illumination

␈↓"β␈↓ α␈↓∧␈↓ αHView.In: View ␈↓βX␈↓∧ Coordinate → TruthValues

␈↓"β␈↓ α␈↓∧␈↓ αHFindPictures: View ␈↓βX␈↓∧ Coordinate → IdList

␈↓"β␈↓ α␈↓∧␈↓ αHDeletePicture: View ␈↓βX␈↓∧ PictureId → View

␈↓"β␈↓ α␈↓∧␈↓ αHAxioms:

␈↓"β␈↓ α␈↓∧␈↓ αHView.Appearance(AddPicture(v, coord', id, p), coord) ␈↓=␈↓∧
␈↓"β␈↓ α␈↓∧␈↓ αH                ␈↓¬if␈↓∧ Picture.In(p, Minus(coord, coord'))
␈↓"β␈↓ α␈↓∧␈↓ αH                ␈↓¬then␈↓∧ Picture.Appearance(p, Minus(coord, coord'))
␈↓"β␈↓ α␈↓∧␈↓ αH                ␈↓¬else␈↓∧ View.Appearance(v, coord)

␈↓"β␈↓ α␈↓∧␈↓ αHView.Appearance(View.Empty, coord)␈↓¬ intentionally left unspecified

␈↓"β␈↓ α␈↓¬␈↓ αH␈↓∧View.In(View.Empty, coord) ␈↓=␈↓∧ False

␈↓"β␈↓ α␈↓∧␈↓ αHView.In(AddPicture(v, coord', id, p), coord) ␈↓=␈↓∧
␈↓"β␈↓ α␈↓∧␈↓ αH                        Picture.In(p, Minus(coord, coord')) ∨ View.In(v, coord)

␈↓"β␈↓ α␈↓∧␈↓ αHFindPictures(View.Empty, coord) ␈↓=␈↓∧ IdList.Empty
␈↓ α␈↓␈↓ β␈↓  5␈↓

␈↓"β␈↓ α␈↓∧␈↓ αHFindPictures(AddPicture(v, coord', id, p), coord) ␈↓=␈↓∧
␈↓"β␈↓ α␈↓∧␈↓ αH                ␈↓¬if␈↓∧ Picture.In(p, Minus(coord, coord'))
␈↓"β␈↓ α␈↓∧␈↓ αH                ␈↓¬then␈↓∧ IdList.Insert(id, FindPictures(v, coord))
␈↓"β␈↓ α␈↓∧␈↓ αH                ␈↓¬else␈↓∧ FindPictures(v, coord)

␈↓"β␈↓ α␈↓∧␈↓ αHDeletePicture(View.Empty, id) ␈↓=␈↓∧ View.Empty

␈↓"β␈↓ α␈↓∧␈↓ αHDeletePicture( AddPicture(v, coord, id', p), id) ␈↓=␈↓∧
␈↓"β␈↓ α␈↓∧␈↓ αH                ␈↓¬if␈↓∧ PictureId.Equal(id, id')
␈↓"β␈↓ α␈↓∧␈↓ αH                ␈↓¬then␈↓∧ v
␈↓"β␈↓ α␈↓∧␈↓ αH                ␈↓¬else␈↓∧ AddPicture(DeletePicture(v, id), coord, id', p)


␈↓"β␈↓ α␈↓↓␈↓ αHGuttag␈αand␈αHorning␈αuse␈αthe␈αconvention␈αof␈αprefixing␈αa␈αfunction␈αname␈αby␈αthe␈αtype␈αit
␈↓ α␈↓↓is␈α
operating␈αon␈α
and␈αa␈α
dot.␈α In␈α
this␈αway␈α
they␈αcan␈α
use␈αthe␈α
same␈αname␈α
for␈α
similar␈αfunctions
␈↓ α␈↓↓being␈αdefined␈αover␈α
several␈αdifferent␈αtypes.␈α
 They␈αchose␈αto␈α
use␈αa␈α0-ary␈αfunction␈α
␈↓View.Empty␈↓↓
␈↓ α␈↓↓to␈α⊃indicate␈α∩the␈α⊃empty␈α⊃view,␈α∩we␈α⊃use␈α∩a␈α⊃constant␈α⊃␈↓αmt-view␈↓↓.␈α∩␈↓AddPicture␈↓↓␈α⊃is␈α∩the␈α⊃constructor
␈↓ α␈↓↓function␈α∞for␈α∞type␈α
␈↓View␈↓↓.␈α∞ ␈↓Appearance␈↓↓␈α∞and␈α
␈↓In␈↓↓␈α∞are␈α∞determined␈α
by␈α∞the␈α∞components␈α
(pictures)
␈↓ α␈↓↓making␈α⊂up␈α∂a␈α⊂view.␈α⊂ ␈↓FindPictures␈↓↓␈α∂is␈α⊂a␈α∂function␈α⊂that␈α⊂constructs␈α∂a␈α⊂list␈α∂of␈α⊂␈↓id␈↓↓'s␈α⊂of␈α∂pictures
␈↓ α␈↓↓containing␈α
a␈α
given␈α
coordinate.␈α∞ ␈↓DeletePicture␈↓↓␈α
deletes␈α
a␈α
picture,␈α∞specified␈α
by␈α
its␈α
␈↓id␈↓↓,␈α∞from␈α
a
␈↓ α␈↓↓view.

␈↓"β␈↓ α␈↓↓␈↓ αHAgain,␈α↔using␈α_Horn␈α↔clauses,␈α_we␈α↔indicate␈α↔the␈α_types␈α↔of␈α_arguments␈α↔only␈α_in␈α↔the
␈↓ α␈↓↓specification␈α⊃of␈α⊃␈↓View␈↓↓,␈α⊃and␈α∩assume␈α⊃the␈α⊃desired␈α⊃types␈α∩are␈α⊃made␈α⊃apparent␈α⊃by␈α∩naming␈α⊃of
␈↓ α␈↓↓variables.


␈↓"β␈↓ α␈↓↓␈↓ αH␈↓∧View(␈↓εmt-view␈↓∧) ←

␈↓"β␈↓ α␈↓∧␈↓ αHView(␈↓εadd-picture␈↓∧(v, c, id, p)) ← View(v), Coordinate(c), PictureId(id), Picture(p)

␈↓"β␈↓ α␈↓∧␈↓ αHView-Appearance(␈↓εmt-view␈↓∧, coord, x) ←

␈↓"β␈↓ α␈↓∧␈↓ αH␈↓¬As in the algebraic specification, we leave unspecified the appearance of the
␈↓"β␈↓ α␈↓¬␈↓ αH␈↓εmt-view␈↓¬ at any coordinate.  Since we have no if-then-else, the axiom describing
␈↓"β␈↓ α␈↓¬␈↓ αH␈↓∧View.Appearance␈↓¬ corresponds to two Horn clauses, one for each alternative.␈↓∧

␈↓"β␈↓ α␈↓∧␈↓ αHView-Appearance(␈↓εadd-picture␈↓∧(v, coord', id, p), coord, illum) ←
␈↓"β␈↓ α␈↓∧␈↓ αH                                Picture-In(p, ␈↓εminus␈↓∧(coord, coord'), ␈↓εtrue␈↓∧),
␈↓"β␈↓ α␈↓∧␈↓ αH                                Picture-Appearance(p, ␈↓εminus␈↓∧(coord, coord'), illum)

␈↓"β␈↓ α␈↓∧␈↓ αHView-Appearance(␈↓εadd-picture␈↓∧(v, coord', id, p), coord, illum) ←
␈↓"β␈↓ α␈↓∧␈↓ αH                                Picture-In(p, ␈↓εminus␈↓∧(coord, coord'), ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧␈↓ αH                                View-Appearance(v, coord, illum)

␈↓"β␈↓ α␈↓∧␈↓ αHView-In(␈↓εmt-view␈↓∧, coord, ␈↓εfalse␈↓∧) ←

␈↓"β␈↓ α␈↓∧␈↓ αH␈↓¬Horn clauses are not allowed alternative conditions. Thus the second axiom for
␈↓"β␈↓ α␈↓¬␈↓ αH␈↓∧View.In␈↓¬ is handled by the following three Horn clauses, one for each alternative
␈↓"β␈↓ α␈↓¬␈↓ αHmaking the conclusion ␈↓εtrue␈↓¬, and a third to enable us to derive the fact that a
␈↓ α␈↓␈↓ β␈↓  6␈↓

␈↓"β␈↓ α␈↓¬␈↓ αHcoordinate is not in a ␈↓∧view␈↓¬.

␈↓"β␈↓ α␈↓¬␈↓ αH␈↓∧View-In(␈↓εadd-picture␈↓∧(v, coord', id, p), coord, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧␈↓ αH                                Picture-In(p, ␈↓εminus␈↓∧(coord, coord'), ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧␈↓ αHView-In(␈↓εadd-picture␈↓∧(v, coord', id, p), coord, ␈↓εtrue␈↓∧) ← View-In(v, coord, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧␈↓ αHView-In(␈↓εadd-picture␈↓∧(v, coord', id, p), coord, ␈↓εfalse␈↓∧) ←
␈↓"β␈↓ α␈↓∧␈↓ αH                                Picture-In(p, ␈↓εminus␈↓∧(coord, coord'), ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧␈↓ αH                                View-In(v, coord, ␈↓εfalse␈↓∧)

␈↓"β␈↓ α␈↓∧␈↓ αHFindPictures(␈↓εmt-view␈↓∧, coord, ␈↓εmt-idlist␈↓∧) ←

␈↓"β␈↓ α␈↓∧␈↓ αHFindPictures(␈↓εadd-picture␈↓∧(v, coord', id, p), coord, ␈↓εidlist-insert␈↓∧(id,idl)) ←
␈↓"β␈↓ α␈↓∧␈↓ αH                                Picture-In(p, ␈↓εminus␈↓∧(coord, coord'), ␈↓εtrue␈↓∧),
␈↓"β␈↓ α␈↓∧␈↓ αH                                FindPictures(v, coord, idl)

␈↓"β␈↓ α␈↓∧␈↓ αHFindPictures(␈↓εadd-picture␈↓∧(v, coord', id, p), coord, idl) ←
␈↓"β␈↓ α␈↓∧␈↓ αH                                Picture-In(p, ␈↓εminus␈↓∧(coord, coord'), ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧␈↓ αH                                FindPictures(v, coord, idl)

␈↓"β␈↓ α␈↓∧␈↓ αHDeletePicture(␈↓εmt-view␈↓∧, id, ␈↓εmt-view␈↓∧) ←

␈↓"β␈↓ α␈↓∧␈↓ αHDeletePicture(␈↓εadd-picture␈↓∧(v, coord, id, p), id, v) ←

␈↓"β␈↓ α␈↓∧␈↓ αHDeletePicture(␈↓εadd-picture␈↓∧(v, coord, id', p), id, ␈↓εadd-picture␈↓∧(v', coord, id', p)) ←
␈↓"β␈↓ α␈↓∧␈↓ αH                                PictureId-equal(id, id', ␈↓εfalse␈↓∧), DeletePicture(v, id, v')

␈↓"β␈↓ α␈↓↓␈↓FindPictures␈↓↓␈α
and␈α
␈↓DeletePicture␈↓↓␈αpresent␈α
no␈α
surprises.␈α
 Again,␈αan␈α
if-then-else␈α
in␈α
an␈αaxiom
␈↓ α␈↓↓results␈α_in␈α↔two␈α_clauses␈α↔in␈α_the␈α_Horn␈α↔clause␈α_specification.␈α↔ A␈α_complete␈α_Horn␈α↔clause
␈↓ α␈↓↓specification of the display is given in the appendix.


␈↓"β␈↓ α␈↓↓␈↓ αHIn␈α
analyzing␈α
the␈α
specification␈α
using␈α
the␈αalgebraic␈α
axioms␈α
one␈α
needs␈α
an␈α
expert␈α
to␈αgo
␈↓ α␈↓↓between␈α
the␈αquestioner␈α
and␈α
the␈αspecification.␈α
 For␈α
example,␈αand␈α
informal␈α
question␈αasked␈α
of
␈↓ α␈↓↓Guttag␈α∀and␈α∀Horning␈α∀was:␈α∀"Is␈α∀it␈α∀the␈α∀case␈α∀that␈α∀pictures␈α∀are␈α∀not␈α∀transparent␈α∀or␈α∪even
␈↓ α␈↓↓translucent?␈α
I.e.,␈α
if␈α
two␈α
pictures␈α
overlap,␈α
does␈αthe␈α
bottom␈α
one␈α
have␈α
no␈α
effect␈α
on␈α
what␈αone
␈↓ α␈↓↓sees␈α⊃through␈α⊃the␈α∩top␈α⊃one?".␈α⊃The␈α∩alternatives␈α⊃are␈α⊃pictured␈α⊃in␈α∩Figures␈α⊃3a␈α⊃and␈α∩3b.␈α⊃The
␈↓ α␈↓↓question was formalized as:

␈↓"β␈↓ α␈↓↓␈↓ αH"Is it true that
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓∧(∀c, c', w, id, v1, v2)[Picture.In(w, Minus(c, c')) →
␈↓"β␈↓ α␈↓∧   [View.Appearance(AddPicture(v1, c', id, w), c) ␈↓=␈↓∧ View.Appearance(AddPicture(v2, c', id, w), c)]] ␈↓¬?"

␈↓"β␈↓ α␈↓↓The␈αformal␈αquestion␈αis␈αanswered␈αaffirmatively,␈αfollowing␈αdirectly␈αfrom␈αthe␈αfirst␈αalternative
␈↓ α␈↓↓in the first axiom of type ␈↓View␈↓↓.

␈↓"β␈↓ α␈↓↓␈↓ αHIf␈α⊃we␈α⊃so␈α⊃desired,␈α⊃we␈α⊃could␈α⊃formalize␈α⊃the␈α⊃question␈α⊃to␈α⊃be␈α⊃put␈α⊃to␈α⊃our␈α⊃Horn␈α⊃clause
␈↓ α␈↓↓specification␈α⊂and␈α⊃derive␈α⊂the␈α⊂same␈α⊃answer,␈α⊂using␈α⊃the␈α⊂second␈α⊂clause␈α⊃in␈α⊂the␈α⊃definition␈α⊂of
␈↓ α␈↓␈↓ ε␈↓  7␈↓

␈↓"β␈↓ α␈↓↓␈↓View-Appearance␈↓↓,␈αbut␈αthere␈α
is␈αno␈αneed.␈α Since␈α
we␈αcan␈αrun␈α
the␈αHorn␈αclause␈αspecification,␈α
all
␈↓ α␈↓↓the␈αuser␈αneed␈αdo␈αis␈αconstruct␈αoverlapping␈αpictures␈αand␈αlook␈αat␈αthe␈αresult.␈αThis␈αis␈αsufficient
␈↓ α␈↓↓to␈αanswer␈αquestions␈αabout␈αspecific␈αcases.␈α If␈αone␈αis␈αinterested␈αin␈αproving␈αgeneral␈αproperties,
␈↓ α␈↓↓then␈α∂we␈α∂must␈α∂fall␈α∂back␈α∂to␈α∂a␈α∂formalization␈α∂of␈α∂the␈α∂question␈α∂and␈α∂formal␈α∂derivation␈α∂of␈α∞an
␈↓ α␈↓↓answer␈α∞from␈α∞the␈α∞specification.␈α∂In␈α∞order␈α∞to␈α∞accomplish␈α∂this␈α∞derivation,␈α∞we␈α∞often␈α∂need␈α∞the
␈↓ α␈↓↓"closed␈α∞world"␈α∞assumption,␈α∞that␈α∞is,␈α∞we␈α∞assume␈α∞that␈α∞the␈α∞specification␈α∞is␈α∞complete.␈α∞ For␈α∞the
␈↓ α␈↓↓current example, the question is formalized as:

␈↓"β␈↓ α␈↓↓␈↓ αH"Is it true that
␈↓"β␈↓ α␈↓↓␈↓ αH␈↓∧View-Appearance(␈↓εadd-picture␈↓∧(v1, c', id, p), c, illum) ←
␈↓"β␈↓ α␈↓∧␈↓ αH        Picture-In(p, ␈↓εminus␈↓∧(c, c', ␈↓εtrue␈↓∧),
␈↓"β␈↓ α␈↓∧␈↓ αH        View-Appearanc(␈↓εadd-picture␈↓∧(v2, c', id, p), c, illum) ␈↓¬?"

␈↓"β␈↓ α␈↓↓By␈α≡assuming␈α≡the␈α≡"only-if"␈α≡direction␈α≡of␈α≥the␈α≡first␈α≡clause␈α≡in␈α≡the␈α≡definition␈α≥of
␈↓ α␈↓↓␈↓View-Appearance␈↓↓,␈α∃which␈α⊗is␈α∃clearly␈α⊗the␈α∃intent␈α∃of␈α⊗the␈α∃definition,␈α⊗we␈α∃can␈α⊗derive␈α∃that
␈↓ α␈↓↓␈↓Picture-Appearance(p,␈α
␈↓αminus␈↓(c,␈α∞c'),␈α
illum)␈↓↓.␈α
Then␈α∞using␈α
the␈α
same␈α∞clause,␈α
exactly␈α∞as␈α
stated,
␈↓ α␈↓↓we derive the result.

␈↓"β␈↓ α␈↓↓␈↓ αHUsing␈α∩Horn␈α∪clauses␈α∩as␈α∩a␈α∪design␈α∩tool␈α∩we␈α∪enjoy␈α∩all␈α∩the␈α∪benefits␈α∩of␈α∪the␈α∩algebraic
␈↓ α␈↓↓approach,␈α
and␈α
gain␈α
the␈αadvantage␈α
that␈α
testing␈α
is␈αmore␈α
easily␈α
accomplished.␈α
 An␈αexpert␈α
may
␈↓ α␈↓↓still␈α
be␈α
required␈αto␈α
develop␈α
the␈αdesign␈α
specification␈α
and␈αto␈α
modify␈α
it␈αif␈α
necessary,␈α
but␈αthe
␈↓ α␈↓↓analysis␈α∞of␈α∞the␈α∞design␈α
can␈α∞be␈α∞carried␈α∞out␈α
by␈α∞people␈α∞who␈α∞may␈α
be␈α∞experts␈α∞in␈α∞the␈α
problem
␈↓ α␈↓↓domain but not in the specification language.



␈↓"β␈↓ α␈↓↓␈↓ ε	␈↓αReferences␈↓↓

␈↓"β␈↓ α␈↓↓[1] Davis, R. E., "Generation of Correct Programs from Logic Specifications",
␈↓"β␈↓ α␈↓↓                Ph.D. Thesis, Board of Information Sciences, University of
␈↓"β␈↓ α␈↓↓                California, Santa Cruz, 1979.

␈↓"β␈↓ α␈↓↓[2] Guttag, J., and J. Horning, "Formal Specification As a Design Tool",
␈↓"β␈↓ α␈↓↓                Proceedings of the ACM Symposium on Principles of Programming
␈↓"β␈↓ α␈↓↓                Languages, 1980.

␈↓"β␈↓ α␈↓↓[3] Kowalski, R., ␈↓Logic for Problem Solving␈↓↓, Elsevier North Holland, Inc., 1979.
␈↓ α␈↓␈↓ β␈↓  8␈↓


␈↓"β␈↓ α␈↓↓␈↓ ε∂␈↓αAppendix␈↓∧

␈↓"β␈↓ α␈↓↓␈↓∧TYPE Picture

␈↓"β␈↓ α␈↓∧Picture(␈↓εmake-picture␈↓∧(cont, bound, trans)) ←
␈↓"β␈↓ α␈↓∧        Contents(cont), Boundary(bound), Translation(trans)

␈↓"β␈↓ α␈↓∧Picture-Appearance(␈↓εmake-picture␈↓∧(cont, bound, trans), coord, illum) ←
␈↓"β␈↓ α␈↓∧        Compute-position(coord, trans, coord'), Contents-appearance(cont, coord', illum),
␈↓"β␈↓ α␈↓∧        Contents(cont), Boundary(bound), Translation(trans), Coordinate(coord),
␈↓"β␈↓ α␈↓∧        Coordinate(coord'), Illumination(illum)

␈↓"β␈↓ α␈↓∧Picture-In(␈↓εmake-picture␈↓∧(cont, bound, trans), coord, tv) ←
␈↓"β␈↓ α␈↓∧        Lies-in(coord, bound, tv), Contents(cont), Boundary(bound),
␈↓"β␈↓ α␈↓∧        Translation(trans), Coordinate(coord), Truth-value(tv)

␈↓"β␈↓ α␈↓∧END TYPE Picture

␈↓"β␈↓ α␈↓∧TYPE Contents

␈↓"β␈↓ α␈↓∧Contents(␈↓εmt-contents␈↓∧) ←

␈↓"β␈↓ α␈↓∧Contents(␈↓εadd-component␈↓∧(cont, comp, coord)) ← Contents(cont), Component(comp), Coordinate(coord)

␈↓"β␈↓ α␈↓∧Contents-Appearance(␈↓εmt-contents␈↓∧, coord, x) ←

␈↓"β␈↓ α␈↓∧␈↓¬The appearance of an empty contents at a coordinate is intentionally left unspecified as yet.␈↓∧

␈↓"β␈↓ α␈↓∧Contents-Appearance(␈↓εadd-component␈↓∧(cont, comp, coord'), coord, illum) ←
␈↓"β␈↓ α␈↓∧        Component-In(comp, ␈↓εminus␈↓∧(coord, coord'), ␈↓εtrue␈↓∧), Contents-In(cont, coord, ␈↓εtrue␈↓∧),
␈↓"β␈↓ α␈↓∧        Component-Appearance(comp, ␈↓εminus␈↓∧(coord, coord'), illum1),
␈↓"β␈↓ α␈↓∧        Contents-Appearance(cont, coord, illum2), Combine(illum1, illum2, illum)

␈↓"β␈↓ α␈↓∧Contents-Appearance(␈↓εadd-component␈↓∧(cont, comp, coord'), coord, illum) ←
␈↓"β␈↓ α␈↓∧        Component-In(comp, ␈↓εminus␈↓∧(coord, coord'), ␈↓εtrue␈↓∧), Contents-In(cont, coord, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Component-Appearance(comp, ␈↓εminus␈↓∧(coord, coord'), illum)

␈↓"β␈↓ α␈↓∧Contents-Appearance(␈↓εadd-component␈↓∧(cont, comp, coord'), coord, illum) ←
␈↓"β␈↓ α␈↓∧        Component-In(comp, ␈↓εminus␈↓∧(coord, coord'), ␈↓εfalse␈↓∧), Contents-Appearance(cont, coord, illum)

␈↓"β␈↓ α␈↓∧Contents-In(␈↓εmt-contents␈↓∧, coord, ␈↓εfalse␈↓∧) ←

␈↓"β␈↓ α␈↓∧Contents-In(␈↓εadd-component␈↓∧(cont, comp, coord'), coord, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Component-In(comp, ␈↓εminus␈↓∧(coord, coord'), ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧Contents-In(␈↓εadd-component␈↓∧(cont, comp, coord'), coord, ␈↓εtrue␈↓∧) ← Contents-In(cont, coord, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧Contents-In(␈↓εadd-component␈↓∧(cont, comp, coord'), coord, ␈↓εfalse␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Component-In(comp, ␈↓εminus␈↓∧(coord, coord'), ␈↓εfalse␈↓∧), Contents-In(cont, coord, ␈↓εfalse␈↓∧)
␈↓ α␈↓␈↓ ∧␈↓  9␈↓

␈↓"β␈↓ α␈↓∧END TYPE Contents
␈↓ α␈↓␈↓ 
w␈↓  10␈↓

␈↓"β␈↓ α␈↓∧TYPE Component
␈↓"β␈↓ α␈↓∧␈↓¬Simply the union of ␈↓∧View, Text␈↓¬, and ␈↓∧Figure.

␈↓"β␈↓ α␈↓∧Component(␈↓εmake-vcomp␈↓∧(view)) ←

␈↓"β␈↓ α␈↓∧Component(␈↓εmake-tcomp␈↓∧(text)) ←

␈↓"β␈↓ α␈↓∧Component(␈↓εmake-fcomp␈↓∧(figure)) ←

␈↓"β␈↓ α␈↓∧Component-Appearance(␈↓εmake-vcomp␈↓∧(view), coord, illum) ←
␈↓"β␈↓ α␈↓∧        View-Appearance(view, coord, illum)

␈↓"β␈↓ α␈↓∧Component-Appearance(␈↓εmake-tcomp␈↓∧(text), coord, illum) ←
␈↓"β␈↓ α␈↓∧        Text-Appearance(text, coord, illum)

␈↓"β␈↓ α␈↓∧Component-Appearance(␈↓εmake-fcomp␈↓∧(figure), coord, illum) ←
␈↓"β␈↓ α␈↓∧        Figure-Appearance(figure, coord, illum)

␈↓"β␈↓ α␈↓∧Component-In(␈↓εmake-vcomp␈↓∧(view), coord, tv) ←
␈↓"β␈↓ α␈↓∧        View-In(view, coord, tv)

␈↓"β␈↓ α␈↓∧Component-In(␈↓εmake-tcomp␈↓∧(text), coord, tv) ←
␈↓"β␈↓ α␈↓∧        Text-In(text, coord, tv)

␈↓"β␈↓ α␈↓∧Component-In(␈↓εmake-fcomp␈↓∧(figure), coord, tv) ←
␈↓"β␈↓ α␈↓∧        Figure-In(figure, coord, tv)

␈↓"β␈↓ α␈↓∧END TYPE Component
␈↓ α␈↓␈↓ 
|␈↓  11␈↓

␈↓"β␈↓ α␈↓∧TYPE View

␈↓"β␈↓ α␈↓∧View(␈↓εmt-view␈↓∧) ←

␈↓"β␈↓ α␈↓∧View(␈↓εadd-picture␈↓∧(view, coord, picture-id, picture)) ←

␈↓"β␈↓ α␈↓∧View-Appearance(␈↓εmt-view␈↓∧, coord, x) ←

␈↓"β␈↓ α␈↓∧␈↓¬Again, we leave unspecified the appearance
␈↓"β␈↓ α␈↓¬of the ␈↓∧mt-view␈↓¬ at any coordinate␈↓∧

␈↓"β␈↓ α␈↓∧View-Appearance(␈↓εadd-picture␈↓∧(v, coord', id, p), coord, illum) ←
␈↓"β␈↓ α␈↓∧        Picture-In(p, ␈↓εminus␈↓∧(coord, coord'), ␈↓εtrue␈↓∧),
␈↓"β␈↓ α␈↓∧        Picture-Appearance(p, ␈↓εminus␈↓∧(coord, coord'), illum)

␈↓"β␈↓ α␈↓∧View-Appearance(␈↓εadd-picture␈↓∧(v, coord', id, p), coord, illum) ←
␈↓"β␈↓ α␈↓∧        Picture-In(p, ␈↓εminus␈↓∧(coord, coord'), ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        View-Appearance(v, coord, illum)

␈↓"β␈↓ α␈↓∧View-In(␈↓εmt-view␈↓∧, coord, ␈↓εfalse␈↓∧) ←

␈↓"β␈↓ α␈↓∧View-In(␈↓εadd-picture␈↓∧(v, coord', id, p), coord, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Picture-In(p, ␈↓εminus␈↓∧(coord, coord'), ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧View-In(␈↓εadd-picture␈↓∧(v, coord', id, p), coord, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        View-In(v, coord, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧View-In(␈↓εadd-picture␈↓∧(v, coord', id, p), coord, ␈↓εfalse␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Picture-In(p, ␈↓εminus␈↓∧(coord, coord'), ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        View-In(v, coord, ␈↓εfalse␈↓∧)

␈↓"β␈↓ α␈↓∧FindPictures(␈↓εmt-view␈↓∧, coord, ␈↓εmt-idlist␈↓∧) ←

␈↓"β␈↓ α␈↓∧FindPictures(␈↓εadd-picture␈↓∧(v, coord', id, p),
␈↓"β␈↓ α␈↓∧                coord, ␈↓εidlist-insert␈↓∧(id, idl)) ←
␈↓"β␈↓ α␈↓∧        Picture-In(p, ␈↓εminus␈↓∧(coord, coord'), ␈↓εtrue␈↓∧),
␈↓"β␈↓ α␈↓∧        FindPictures(v, coord, idl)

␈↓"β␈↓ α␈↓∧FindPictures(␈↓εadd-picture␈↓∧(v, coord', id, p), coord, idl) ←
␈↓"β␈↓ α␈↓∧        Picture-In(p, ␈↓εminus␈↓∧(coord, coord'), ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        FindPictures(v, coord, idl)

␈↓"β␈↓ α␈↓∧DeletePicture(␈↓εmt-view␈↓∧, id, ␈↓εmt-view␈↓∧) ←

␈↓"β␈↓ α␈↓∧DeletePicture(␈↓εadd-picture␈↓∧(v, coord, id, p), id, v) ←

␈↓"β␈↓ α␈↓∧DeletePicture(␈↓εadd-picture␈↓∧(v, coord, id', p),
␈↓"β␈↓ α␈↓∧                id, ␈↓εadd-picture␈↓∧(v', coord, id', p)) ←
␈↓"β␈↓ α␈↓∧        PictureId-equal(id, id', ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        DeletePicture(v, id, v')
␈↓ α␈↓␈↓ 
w␈↓  12␈↓

␈↓"β␈↓ α␈↓∧END TYPE View
␈↓ α␈↓␈↓ 
v␈↓  13␈↓

␈↓"β␈↓ α␈↓∧TYPE Idlist

␈↓"β␈↓ α␈↓∧Idlist(␈↓εmt-idlist␈↓∧) ←

␈↓"β␈↓ α␈↓∧Idlist(␈↓εidlist-insert␈↓∧(id, idl)) ←
␈↓"β␈↓ α␈↓∧                 PictureId(id), Idlist(idl)

␈↓"β␈↓ α␈↓∧END TYPE Idlist

␈↓"β␈↓ α␈↓∧TYPE Text

␈↓"β␈↓ α␈↓∧Text(␈↓εmt-text␈↓∧) ←

␈↓"β␈↓ α␈↓∧Text(␈↓εtext-insert␈↓∧(par, txt)) ← Paragraph(par), Text(txt)

␈↓"β␈↓ α␈↓∧␈↓¬macro: ␈↓∧down(d)␈↓¬ is ␈↓∧minus(coord, times(d, ␈↓εunitvectordown␈↓∧)

␈↓"β␈↓ α␈↓∧Text-Appearance(␈↓εmt-text␈↓∧, coord, x) ←

␈↓"β␈↓ α␈↓∧Text-Appearance(␈↓εtext-insert␈↓∧(par, txt), coord, illum) ←
␈↓"β␈↓ α␈↓∧        Paragraph-In(par, coord, ␈↓εtrue␈↓∧),
␈↓"β␈↓ α␈↓∧        Paragraph-Appearance(p, coord, illum)

␈↓"β␈↓ α␈↓∧Text-Appearance(␈↓εtext-insert␈↓∧(par, txt), coord, illum) ←
␈↓"β␈↓ α␈↓∧        Paragraph-In(par, coord, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Paragraph-Height(par, d),
␈↓"β␈↓ α␈↓∧        Text-Appearance(txt, ␈↓εdown␈↓∧(d), illum)

␈↓"β␈↓ α␈↓∧Text-In(␈↓εmt-text␈↓∧, coord, ␈↓εfalse␈↓∧) ←

␈↓"β␈↓ α␈↓∧Text-In(␈↓εtext-insert␈↓∧(par, txt), coord, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Paragraph-In(par, coord, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧Text-In(␈↓εtext-insert␈↓∧(par, txt), coord, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Paragraph-Height(par, d),
␈↓"β␈↓ α␈↓∧        Text-In(txt, ␈↓εdown␈↓∧(d), ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧Text-In(␈↓εtext-insert␈↓∧(par, txt), coord, ␈↓εfalse␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Paragraph-In(par, coord, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Paragraph-Height(par, d),
␈↓"β␈↓ α␈↓∧        Text-In(txt, ␈↓εdown␈↓∧(d), ␈↓εfalse␈↓∧)

␈↓"β␈↓ α␈↓∧END TYPE Text
␈↓ α␈↓␈↓ 
y␈↓  14␈↓

␈↓"β␈↓ α␈↓∧TYPE Paragraph
␈↓"β␈↓ α␈↓∧␈↓¬macro: ␈↓εdown␈↓¬(d) is ␈↓εminus␈↓¬(coord, ␈↓εtimes␈↓¬(d, ␈↓εunitvectordown␈↓¬) ␈↓∧

␈↓"β␈↓ α␈↓∧Paragraph(␈↓εmake-paragraph␈↓∧(parlooks, eng-string)) ←

␈↓"β␈↓ α␈↓∧Par-Firstline(␈↓εmake-paragraph␈↓∧(look, s), line) ←
␈↓"β␈↓ α␈↓∧        Parlooks-width(look, w),
␈↓"β␈↓ α␈↓∧        EngString-Firstline(s, w, line)

␈↓"β␈↓ α␈↓∧Par-Balance(␈↓εmake-paragraph␈↓∧(look, s),
␈↓"β␈↓ α␈↓∧             ␈↓εmake-paragraph␈↓∧(look, s')) ←
␈↓"β␈↓ α␈↓∧        Parlooks-width(look, w),
␈↓"β␈↓ α␈↓∧        EngString-Balance(s, w)

␈↓"β␈↓ α␈↓∧Par-Null(␈↓εmake-paragraph␈↓∧(look, s), tv) ←
␈↓"β␈↓ α␈↓∧        String-Null(s, tv)

␈↓"β␈↓ α␈↓∧Par-Space(␈↓εmake-paragraph␈↓∧(look, s), dist) ←
␈↓"β␈↓ α␈↓∧                ParLooks-space(look, dist)

␈↓"β␈↓ α␈↓∧Par-Height(p, dist) ←
␈↓"β␈↓ α␈↓∧        Par-Null(p, ␈↓εtrue␈↓∧), Par-Space(p, dist)

␈↓"β␈↓ α␈↓∧Par-Height(p, dist1 + dist2) ← Par-Null(p, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Par-Firstline(p, line), Line-Height(line, dist1),
␈↓"β␈↓ α␈↓∧        Par-Balance(p, p'), Par-Height(p', dist2)

␈↓"β␈↓ α␈↓∧Par-In(p, coord, ␈↓εtrue␈↓∧) ← Par-Null(p, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Par-Firstline(p, line), Par-Space(p, dist1),
␈↓"β␈↓ α␈↓∧        Line-Ascent(line, dist2),
␈↓"β␈↓ α␈↓∧        Line-In(line, ␈↓εdown␈↓∧(dist1 + dist2), ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧Par-In(p, coord, ␈↓εtrue␈↓∧) ← Par-Null(p, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Par-Balance(p, p'), Par-Firstline(p, line),
␈↓"β␈↓ α␈↓∧        Line-Height(line, dist), Par-In(p', ␈↓εdown␈↓∧(dist), ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧Par-In(p, coord, ␈↓εfalse␈↓∧) ← Par-Null(p, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧Par-In(p, coord, ␈↓εfalse␈↓∧) ← Par-Null(p, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Par-Firstline(p, line), Par-Space(p, dist1),
␈↓"β␈↓ α␈↓∧        Line-Ascent(line, dist2), Par-Balance(p, p'),
␈↓"β␈↓ α␈↓∧        Line-In(line, ␈↓εdown␈↓∧(dist1 + dist2), ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Line-Height(line, dist), Par-In(p', ␈↓εdown␈↓∧(dist), ␈↓εfalse␈↓∧)

␈↓"β␈↓ α␈↓∧Par-Appearance(p, coord, illum) ←
␈↓"β␈↓ α␈↓∧        Par-Firstline(p, line), Par-Space(p, dist1),
␈↓"β␈↓ α␈↓∧        Line-Ascent(line, dist2),
␈↓"β␈↓ α␈↓∧        Line-In(line, ␈↓εdown␈↓∧(dist1 + dist2), ␈↓εtrue␈↓∧),
␈↓"β␈↓ α␈↓∧        Line-Appearance(line, ␈↓εdown␈↓∧(dist1 + dist2), illum)

␈↓"β␈↓ α␈↓∧Par-Appearance(p, coord, illum) ←
␈↓"β␈↓ α␈↓∧        Par-Firstline(p, line), Par-Space(p, dist1),
␈↓ α␈↓␈↓ 
w␈↓  15␈↓

␈↓"β␈↓ α␈↓∧        Line-Ascent(line, dist2),
␈↓"β␈↓ α␈↓∧        Line-In(line, ␈↓εdown␈↓∧(dist1 + dist2), ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Par-Balance(p, p'), Line-Height(line, dist),
␈↓"β␈↓ α␈↓∧        Par-Appearance(p', ␈↓εdown␈↓∧(dist), illum)

␈↓"β␈↓ α␈↓∧END TYPE PARAGRAPH
␈↓ α␈↓␈↓ 
w␈↓  16␈↓

␈↓"β␈↓ α␈↓∧TYPE EnglishString

␈↓"β␈↓ α␈↓∧EngString(␈↓εmt-string␈↓∧) ←

␈↓"β␈↓ α␈↓∧EngString(␈↓εstring-insert␈↓∧(char, string) ←
␈↓"β␈↓ α␈↓∧        Character(char), EngString(string)

␈↓"β␈↓ α␈↓∧EngString-Firstline(␈↓εmt-string␈↓∧, dist, ␈↓εmt-line␈↓∧) ←

␈↓"β␈↓ α␈↓∧EngString-Firstline(␈↓εstring-insert␈↓∧(c, s), d, c) ←
␈↓"β␈↓ α␈↓∧        SplitHere(s, c, d, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧EngString-Firstline(␈↓εstring-insert␈↓∧(c, s), d,
␈↓"β␈↓ α␈↓∧                        ␈↓εline-insert␈↓∧(c, line)) ←
␈↓"β␈↓ α␈↓∧        SplitHere(s, c, d, ␈↓εfalse␈↓∧), Character-width(c, w),
␈↓"β␈↓ α␈↓∧        EngString-Firstline(s, d-w, line)

␈↓"β␈↓ α␈↓∧EngString-Balance(␈↓εmt-string␈↓∧, d, ␈↓εmt-string␈↓∧)←

␈↓"β␈↓ α␈↓∧EngString-Balance(␈↓εstring-insert␈↓∧(c, s), d, s) ←
␈↓"β␈↓ α␈↓∧        SplitHere(s, c, d, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧EngString-Balance(␈↓εstring-insert␈↓∧(c, s), d, str) ←
␈↓"β␈↓ α␈↓∧        Character-width(c, w), EngString-Balance(s, d-w, str)

␈↓"β␈↓ α␈↓∧SplitHere(␈↓εmt-string␈↓∧, c, d, ␈↓εtrue␈↓∧) ←

␈↓"β␈↓ α␈↓∧SplitHere(␈↓εstring-insert␈↓∧(c', s), c, d, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Character-Equal(c', ␈↓εreturn␈↓∧, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧SplitHere(␈↓εstring-insert␈↓∧(c', s), c, d, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Character-Equal(c', ␈↓εspace␈↓∧, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Character-width(c, w), Character-width(c', w'),
␈↓"β␈↓ α␈↓∧        LessThan(d, w+w', ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧SplitHere(␈↓εstring-insert␈↓∧(c', s), c, d, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        LexicalBreak(c, c', ␈↓εtrue␈↓∧), Character-width(c, w),
␈↓"β␈↓ α␈↓∧        WordFits(s, c', d-w, ␈↓εfalse␈↓∧)

␈↓"β␈↓ α␈↓∧SplitHere(␈↓εstring-insert␈↓∧(c', s), c, d, ␈↓εfalse␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Character-Equal(c', ␈↓εreturn␈↓∧, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Character-Equal(c', ␈↓εspace␈↓∧, tv1),
␈↓"β␈↓ α␈↓∧        Character-width(c, w), Character-width(c', w'),
␈↓"β␈↓ α␈↓∧        LessThan(d, w+w', tv2), Not(tv2, tv2'),
␈↓"β␈↓ α␈↓∧        Or(tv1, tv2', ␈↓εtrue␈↓∧),
␈↓"β␈↓ α␈↓∧        LexicalBreak(c, c', tv3), Not(tv3, tv3'),
␈↓"β␈↓ α␈↓∧        Character-width(c, w), WordFits(s, c', d-w, tv4),
␈↓"β␈↓ α␈↓∧        Or(tv3', tv4, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧Not(␈↓εtrue␈↓∧, ␈↓εfalse␈↓∧) ←

␈↓"β␈↓ α␈↓∧Not(␈↓εfalse␈↓∧, ␈↓εtrue␈↓∧) ←
␈↓ α␈↓␈↓ 
z␈↓  17␈↓

␈↓"β␈↓ α␈↓∧Or(␈↓εtrue␈↓∧, tv, ␈↓εtrue␈↓∧) ←

␈↓"β␈↓ α␈↓∧Or(tv, ␈↓εtrue␈↓∧, ␈↓εtrue␈↓∧) ←

␈↓"β␈↓ α␈↓∧Or(␈↓εfalse␈↓∧, ␈↓εfalse␈↓∧, ␈↓εfalse␈↓∧) ←

␈↓"β␈↓ α␈↓∧LexicalBreak(current, next, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Character-Equal(current, ␈↓εspace␈↓∧, ␈↓εtrue␈↓∧),
␈↓"β␈↓ α␈↓∧        Character-Equal(next, ␈↓εspace␈↓∧, ␈↓εfalse␈↓∧)

␈↓"β␈↓ α␈↓∧LexicalBreak(current, next, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Character-Equal(current, ␈↓εhyphen␈↓∧, ␈↓εtrue␈↓∧),
␈↓"β␈↓ α␈↓∧        Character-Equal(next, ␈↓εhyphen␈↓∧, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Character-Equal(next, ␈↓εspace␈↓∧, ␈↓εfalse␈↓∧)

␈↓"β␈↓ α␈↓∧LexicalBreak(current, next, ␈↓εfalse␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Character-Equal(next, ␈↓εspace␈↓∧, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧LexicalBreak(current, next, ␈↓εfalse␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Character-Equal(current, ␈↓εspace␈↓∧, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Character-Equal(current, ␈↓εhyphen␈↓∧, ␈↓εfalse␈↓∧)

␈↓"β␈↓ α␈↓∧LexicalBreak(current, next, ␈↓εfalse␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Character-Equal(current, ␈↓εspace␈↓∧, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Character-Equal(next, ␈↓εhyphen␈↓∧, ␈↓εtrue␈↓∧),

␈↓"β␈↓ α␈↓∧WordFits(␈↓εmt-string␈↓∧, c, d, ␈↓εtrue␈↓∧) ←

␈↓"β␈↓ α␈↓∧WordFits(␈↓εstring-insert␈↓∧(c', s), c, d, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Character-Equal(c, ␈↓εreturn␈↓∧, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧WordFits(␈↓εstring-insert␈↓∧(c', s), c, d, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Character-Equal(c, ␈↓εspace␈↓∧, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧WordFits(␈↓εstring-insert␈↓∧(c', s), c, d, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        LexicalBreak(c, c', ␈↓εtrue␈↓∧), Character-width(c, w),
␈↓"β␈↓ α␈↓∧        LessThan(d, w, ␈↓εfalse␈↓∧)

␈↓"β␈↓ α␈↓∧WordFits(␈↓εstring-insert␈↓∧(c', s), c, d, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Character-width(c, w), Character-width(c', w'),
␈↓"β␈↓ α␈↓∧        LessThan(d, w+w', ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        WordFits(s, c', d-w, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧WordFits(␈↓εstring-insert␈↓∧(c', s), c, d, ␈↓εfalse␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Character-Equal(c, ␈↓εreturn␈↓∧, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Character-Equal(c, ␈↓εspace␈↓∧, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        LexicalBreak(c, c', tv1), Not(tv1, tv1'),
␈↓"β␈↓ α␈↓∧        Character-width(c, w), LessThan(d, w, tv2),
␈↓"β␈↓ α␈↓∧        Or(tv1', tv2), Character-width(c', w'),
␈↓"β␈↓ α␈↓∧        LessThan(d, w+w', tv3),
␈↓"β␈↓ α␈↓∧        WordFits(s, c', d-w, tv4), Not(tv4, tv4'),
␈↓"β␈↓ α␈↓∧        Or(tv3, tv4', ␈↓εtrue␈↓∧)
␈↓ α␈↓␈↓ 
w␈↓  18␈↓

␈↓"β␈↓ α␈↓∧String-Null(␈↓εmt-string␈↓∧, ␈↓εtrue␈↓∧) ←

␈↓"β␈↓ α␈↓∧String-Null(␈↓εstring-insert␈↓∧(c, s), ␈↓εfalse␈↓∧) ←

␈↓"β␈↓ α␈↓∧END TYPE EnglishString
␈↓ α␈↓␈↓ 
x␈↓  19␈↓

␈↓"β␈↓ α␈↓∧TYPE LINE

␈↓"β␈↓ α␈↓∧Line(␈↓εmt-line␈↓∧) ←

␈↓"β␈↓ α␈↓∧Line(␈↓εline-insert*(c, l)) ← Character(c), Line(l)

␈↓"β␈↓ α␈↓ε␈↓∧Line-Appearance(␈↓εmt-line␈↓∧, coord, illum)␈↓¬
␈↓"β␈↓ α␈↓¬   intentionally left unspecified
␈↓"β␈↓ α␈↓¬macro: ␈↓∧Right(d)␈↓¬ is ␈↓∧Minus(coord, ␈↓εtimes␈↓∧(d, ␈↓εunitvectorright␈↓∧)

␈↓"β␈↓ α␈↓∧Line-Appearance(␈↓εline-insert*(c, ln), coord, illum) ←
␈↓"β␈↓ α␈↓ε        Character-In(c, coord, true),
␈↓"β␈↓ α␈↓ε        Character-Appearance(c, coord, illum)

␈↓"β␈↓ α␈↓εLine-Appearance(line-insert*(c, ln), coord, illum) ←
␈↓"β␈↓ α␈↓ε        Character-In(c, coord, false), Character-width(c, w),
␈↓"β␈↓ α␈↓ε        Line-Appearance(ln, right(w), illum)

␈↓"β␈↓ α␈↓εLine-In(mt-line, coord, false) ←

␈↓"β␈↓ α␈↓εLine-In(line-insert*(c, ln), coord, true) ←
␈↓"β␈↓ α␈↓ε        Character-In(c, coord, true)

␈↓"β␈↓ α␈↓εLine-In(line-insert*(c, ln), coord, true) ←
␈↓"β␈↓ α␈↓ε        Character-width(c, w),
␈↓"β␈↓ α␈↓ε        Line-In(ln, right(w), true)

␈↓"β␈↓ α␈↓εLine-Height(ln, d1+d2) ←
␈↓"β␈↓ α␈↓ε        Line-Ascent(ln, d1), Line-Descent(ln, d2)

␈↓"β␈↓ α␈↓εLine-Ascent(mt-line, 0) ←

␈↓"β␈↓ α␈↓εLine-Ascent(line-insert*(c, ln), d) ←
␈↓"β␈↓ α␈↓ε        Character-Ascent(c, d1), Line-Ascent(ln, d2),
␈↓"β␈↓ α␈↓ε        Maximum(d1, d2, d)

␈↓"β␈↓ α␈↓εLine-Descent(mt-line, 0) ←

␈↓"β␈↓ α␈↓εLine-Descent(line-insert*(c, ln), d) ←
␈↓"β␈↓ α␈↓ε        Character-Descent(c, d1), Line-Descent(ln, d2),
␈↓"β␈↓ α␈↓ε        Maximum(d1, d2, d)

␈↓"β␈↓ α␈↓εMaximum(x, y, x) ← LessThan(x, y, false)

␈↓"β␈↓ α␈↓εMaximum(x, y, y) ← LessThan(y, x, false)

␈↓"β␈↓ α␈↓ε␈↓¬I have assumed the existence of a ␈↓∧LessThan␈↓¬
␈↓"β␈↓ α␈↓¬ predicate that returns ␈↓∧true␈↓¬ or ␈↓∧false

␈↓"β␈↓ α␈↓∧END TYPE LINE
␈↓ α␈↓␈↓ 
r␈↓  20␈↓

␈↓"β␈↓ α␈↓∧TYPE Character

␈↓"β␈↓ α␈↓∧Character(␈↓εmake-char␈↓∧(code, fig, ascent, descent, width)) ←
␈↓"β␈↓ α␈↓∧        CharacterCode(code), Figure(fig), Distance(ascent),
␈↓"β␈↓ α␈↓∧        Distance(descent), Distance(width)

␈↓"β␈↓ α␈↓∧Character-width(␈↓εmake-char␈↓∧(code, fig, ascent,
␈↓"β␈↓ α␈↓∧                                descent, width), width) ←

␈↓"β␈↓ α␈↓∧Char-equal(␈↓εmake-char␈↓∧(code, fig, asc, des, w),
␈↓"β␈↓ α␈↓∧           ␈↓εmake-char␈↓∧(code', fig', asc', des', w')) ←
␈↓"β␈↓ α␈↓∧        CharacterCode-Equal(code, code', ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧Character-Ascent(␈↓εmake-char␈↓∧(code, fig, ascent,
␈↓"β␈↓ α␈↓∧                                descent, width), ascent) ←

␈↓"β␈↓ α␈↓∧Character-Descent(␈↓εmake-char␈↓∧(code, fig, ascent,
␈↓"β␈↓ α␈↓∧                                descent, width), descent) ←

␈↓"β␈↓ α␈↓∧Char-Appearance(␈↓εmake-char␈↓∧(cd, f, a, d, w), coord, illum) ←
␈↓"β␈↓ α␈↓∧        Figure-Appearance(f, coord, illum)

␈↓"β␈↓ α␈↓∧Char-In(␈↓εmake-char␈↓∧(cd, f, a, d, w), coord, ␈↓εtrue␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Figure-In(f, coord, ␈↓εtrue␈↓∧),
␈↓"β␈↓ α␈↓∧        Increasing(a, ␈↓εproject␈↓∧(coord, ␈↓εunitvectordown␈↓∧), d, ␈↓εtrue␈↓∧),
␈↓"β␈↓ α␈↓∧        Increasing(0, ␈↓εproject␈↓∧(coord, ␈↓εunitvectorright␈↓∧), w, ␈↓εtrue␈↓∧)

␈↓"β␈↓ α␈↓∧Char-In(␈↓εmake-char␈↓∧(cd, f, a, d, w), coord, ␈↓εfalse␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Figure-In(f, coord, ␈↓εfalse␈↓∧)

␈↓"β␈↓ α␈↓∧Char-In(␈↓εmake-char␈↓∧(cd, f, a, d, w), coord, ␈↓εfalse␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Increasing(a, ␈↓εproject␈↓∧(coord, ␈↓εunitvectordown␈↓∧), d, ␈↓εfalse␈↓∧)

␈↓"β␈↓ α␈↓∧Char-In(␈↓εmake-char␈↓∧(cd, f, a, d, w), coord, ␈↓εfalse␈↓∧) ←
␈↓"β␈↓ α␈↓∧        Increasing(0, ␈↓εproject␈↓∧(coord, ␈↓εunitvectorright␈↓∧), w, ␈↓εfalse␈↓∧)

␈↓"β␈↓ α␈↓∧END TYPE Character
␈↓ α␈↓␈↓ 
w␈↓  21␈↓

␈↓"β␈↓ α␈↓∧TYPE Figure

␈↓"β␈↓ α␈↓∧␈↓¬Type ␈↓∧Figure␈↓¬ will necessarily include specifications
␈↓"β␈↓ α␈↓¬of the ␈↓∧Appearance␈↓¬ and ␈↓∧In␈↓¬ predicates for the type.
␈↓"β␈↓ α␈↓¬This type is left unspecified as it may be dependent upon
␈↓"β␈↓ α␈↓¬the target system.  Clearly, a more flexible specification
␈↓"β␈↓ α␈↓¬of ␈↓∧Figure␈↓¬ is possible for a bit mapped display than is
␈↓"β␈↓ α␈↓¬possible given a character mapped display. ␈↓∧

␈↓"β␈↓ α␈↓∧END TYPE Figure

␈↓"β␈↓ α␈↓∧TYPE Coordinate

␈↓"β␈↓ α␈↓∧␈↓¬ This type is not yet specified. It needs at least the
␈↓"β␈↓ α␈↓¬functions ␈↓εminus␈↓¬, ␈↓εtimes␈↓¬, and ␈↓εproject␈↓¬, and the constants
␈↓"β␈↓ α␈↓¬␈↓εunitvectorright␈↓¬ and ␈↓εunitvectordown␈↓¬.  A 2-dimensional
␈↓"β␈↓ α␈↓¬vector space would do, and one might consider this a
␈↓"β␈↓ α␈↓¬primitive type of the system one is using.␈↓∧

␈↓"β␈↓ α␈↓∧END TYPE Coordinate

␈↓"β␈↓ α␈↓∧TYPE Distance

␈↓"β␈↓ α␈↓∧␈↓¬ Again, this type should be available already on the
␈↓"β␈↓ α␈↓¬target system.  One simply needs to define the mapping
␈↓"β␈↓ α␈↓¬from the predicate form used in the Horn clauses to
␈↓"β␈↓ α␈↓¬the functions available.␈↓∧

␈↓"β␈↓ α␈↓∧END TYPE Distance

␈↓"β␈↓ α␈↓∧TYPE Font

␈↓"β␈↓ α␈↓∧Font(␈↓εmt-font␈↓∧) ←

␈↓"β␈↓ α␈↓∧Font(␈↓εadd-character␈↓∧(font, char)) ←

␈↓"β␈↓ α␈↓∧Lookup(␈↓εmt-font␈↓∧, code, x) ←
␈↓"β␈↓ α␈↓∧␈↓¬another unspecified pathological case␈↓∧

␈↓"β␈↓ α␈↓∧Lookup(␈↓εadd-character␈↓∧(fnt, ␈↓εmake-char␈↓∧(cd, f, a, d, w)),
␈↓"β␈↓ α␈↓∧                     cd, ␈↓εmake-char␈↓∧(cd, f, a, d, w)) ←

␈↓"β␈↓ α␈↓∧Lookup(␈↓εadd-character␈↓∧(fnt, ␈↓εmake-char␈↓∧(cd, f, a, d, w)), code, c) ←
␈↓"β␈↓ α␈↓∧        CharacterCode-Equal(cd, code, ␈↓εfalse␈↓∧),
␈↓"β␈↓ α␈↓∧        Lookup(fnt, code, c)

␈↓"β␈↓ α␈↓∧END TYPE Font

␈↓"β␈↓ α␈↓∧PRIMITIVES

␈↓"β␈↓ α␈↓∧␈↓¬The primitive predicates that relate the logic to a
␈↓ α␈↓␈↓ 
r␈↓  22␈↓

␈↓"β␈↓ α␈↓¬particular system include the types ␈↓∧Boundary, Translation,
␈↓"β␈↓ α␈↓∧Coordinate, Illumination,␈↓¬ and the predicates, such as
␈↓"β␈↓ α␈↓¬␈↓∧Compute-Position, Lies-In,␈↓¬ and ␈↓∧Minus␈↓¬, that operate
␈↓"β␈↓ α␈↓¬on them. For example, an ␈↓∧illumination␈↓¬ may be one of two
␈↓"β␈↓ α␈↓¬values (white/black), one of several shades of grey, or a
␈↓"β␈↓ α␈↓¬more complex combination of hue and intensity, depending
␈↓"β␈↓ α␈↓¬on the capabilities of the system one is designing.
␈↓ α␈↓␈↓ 
q␈↓  23␈↓